p:. prime(p)  (a1, a2:. p | a1a2  p | a1  p | a2) 

latex

Definitions	P  Q, b | a, prime(a), x:A. B(x), t  T, Dec(P), P  Q, P  Q, P & Q, P  Q, A, False
Lemmas	coprime prod, coprime iff ndivides, decidable divides, prime wf, divides wf